$\forall$${\it the\_es}$:event\_system\{i:l\}. wellfounded\{i:l\}(es{-}E(${\it the\_es}$); $x$,$y$.es{-}locl(${\it the\_es}$; $x$; $y$))